/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Comparator;
import java.util.Iterator;
import java.util.List;
import java.util.Random;
import java.util.Set;
import java.util.TreeSet;

import alloy.ast.LeafId;
import alloy.bool.BooleanFormula;
import alloy.transl.ASTInfo;
import alloy.transl.ExprTransl;
import alloy.transl.IntTransl;
import alloy.transl.RelationAllocator;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.MultiDimIter;
import alloy.util.Params;
import alloy.util.PermIter;
import alloy.util.Util;

/**
 * A {@link SymmetryBreakingMethod} that breaks symmetry by ordering the
 * Boolean variables (thus treating Alloy instances as binary strings)
 * and choosing the lex-leader in each group of isomorphic instances.
 * <p>
 * Right now we only break symmetries that interchange two adjacent atoms
 * of a {@link BasicType}.
 * @see http://ilya.cc/symmetry
 *
 * to-do:
 *   check that the use of MultiDimIterator in _breakOneSymmetry leads to the correct
 *   row- and column- sorting -- probably, shouldn't rely on it.
 *
 *   if doing special-case symmetry-breaking for singletons, consider also
 *   the rows of functional relations -- each row (or column) is a singleton set.
 */
class SBM_LexLeader extends SymmetryBreakingMethod {

    /**
     * Ordering of relations (by their {@link LeafId}s).  Determined b y {@link #getRelationOrder}
     * and use by {@link #_breakOneSymmetry} to construct lex-leader comparators.
     */
    private List /* of LeafId */ _relOrder;

    //////////////
    // Methods //
    ////////////

    SBM_LexLeader(ASTInfo astInfo_, RelationAllocator relAlloc_) {
        super(astInfo_, relAlloc_);
    }

    /**
     * Compute a lex-leader symmetry-breaking predicate.  For each of the {@link BasicType}s
     * in <code>basicTypes_</code>, for each {@link AtomSet} of interchangeable atoms,
     * we break symmetries interchanging adjacent atoms in the group with Crawford's
     * lex-leader method.  We also break some randomly-generated symmetries (up to the value
     * of SYMM.percrand global parameter, as a fraction of the total number of symmetries,
     * and up to the value of the SYMM.maxrand parameter)
     */
    SymmetryBreakingPredicate breakSymmetry(AvailableSymmetry availSymm_,
                        Set/*<BasicType>*/ basicTypes_) {
        SymmetryBreakingPredicate sbp = new SymmetryBreakingPredicate();

        Set /* of Symmetry */ symmsBroken = new TreeSet();
        _breakExchAdjAtomsSymmetries(availSymm_, basicTypes_, sbp, symmsBroken);
        _breakRandomSymmetries(availSymm_, basicTypes_, sbp, symmsBroken);
        // record the symmetry we have broken
        for (Iterator btypeIter = basicTypes_.iterator(); btypeIter.hasNext();) {
            BasicType btype = (BasicType)btypeIter.next();
            availSymm_.removeAllSymmetry(btype);
        }
        return sbp;
    }  // breakSymmetry()

    /** Break "interchange adjacent atoms" symmetries */
    private void _breakExchAdjAtomsSymmetries(AvailableSymmetry availSymm_,
                          Set/*<BasicType>*/ basicTypes_,
                          SymmetryBreakingPredicate sbp_,
                          Set/*<Symmetry>*/ symmsBroken_) {
        for (Iterator btIter = basicTypes_.iterator(); btIter.hasNext();) {
            BasicType btype = (BasicType)btIter.next();
            Set /* of AtomSet */ symmSets = availSymm_.getSymmSets(btype);
            for (Iterator symmSetIter = symmSets.iterator(); symmSetIter.hasNext();) {
            AtomSet symmSet = (AtomSet)symmSetIter.next();
            Integer prevAtom = null;
            for (Iterator atomIter = symmSet.atoms().iterator(); atomIter.hasNext();) {
                Integer curAtom = (Integer)atomIter.next();
                if (prevAtom != null) {
                Symmetry switchAtomsSymm =
                    Symmetry.createTransposition(btype, prevAtom.intValue(), curAtom.intValue());
                sbp_.conjoin(_breakOneSymmetry(switchAtomsSymm));
                symmsBroken_.add(switchAtomsSymm);
                }
                prevAtom = curAtom;
            }
            }  // loop over interchangeable atom sets of a basic type
        }  // loop over basic types
    }  // _breakExchAdjAtomsSymmetries()

    /**
     * Break some random symmetries.   Symmetries are chosen at random from all symmetries with replacement,
     * but each given symmetry is broken only once.  That is, if we randomly choose a symmetry we've already
     * broken, we go and choose another random symmetry, repeating this until we find one we haven't
     * broken yet.
     */
    private void _breakRandomSymmetries(AvailableSymmetry availSymm_,
                    Set /* of BasicType */ basicTypes_,
                    SymmetryBreakingPredicate sbp_,
                    Set /* of Symmetry */ symmsBroken_) {
    // Count the total number of symmetries, and collect a linear list
    // of building blocks out of which we build the symmetries.  Each building
    // block is a symmset -- a set of symmetric (interchangeable) atoms in one BasicType.
    // To generate a random symmetry, we generate a random permutation of each symmset,
    // and compose the permutations to get a symmetry.
    long totalSymms = 1;
    int maxSymmSetSize = 0;
    for (Iterator btIter = basicTypes_.iterator(); btIter.hasNext();) {
        BasicType btype = (BasicType)btIter.next();
        Set /* of AtomSet */ symmSets = availSymm_.getSymmSets(btype);
        for (Iterator symmSetIter = symmSets.iterator(); symmSetIter.hasNext();) {
        AtomSet symmSet = (AtomSet)symmSetIter.next();
        int symmSetSize = symmSet.size();
        maxSymmSetSize = Math.max(maxSymmSetSize, symmSetSize);
        totalSymms *= Util.fact(symmSetSize);
	if (totalSymms > 10000)
	    break;
        }  // loop over symmsets in one basic type
    }  // loop over basic types

    // Decide how many random symmetries we will generate
    long numRandSymms = Math.min(totalSymms,
                    Math.min(Params.glob.getLongParam("SYMM","maxrand"),
                         (long)(((double)Params.glob.getIntParam("SYMM","percrand")) / 100.0
                           * ((double)totalSymms))));
    Dbg.info("Breaking " + numRandSymms + " random symmetries...");
    long randSeed = Params.glob.getLongParam("MAIN", "randseed");
    Random rand = randSeed==0 ? new Random() : new Random(randSeed);
    int[] symmSetPerm = new int[maxSymmSetSize];
    while (numRandSymms > 0) {
        // Generate a random permutation of each symmset,
        // and compose them to obtain a random symmetry.
        Symmetry randSymm = new Symmetry();

        for (Iterator btIter = basicTypes_.iterator(); btIter.hasNext();) {
        BasicType btype = (BasicType)btIter.next();
        int[] btypePerm = new int[btype.getScope()];
        for (int i=0; i<btypePerm.length; i++)
            btypePerm[i] = i;
        Set /* of AtomSet */ symmSets = availSymm_.getSymmSets(btype);
        for (Iterator symmSetIter = symmSets.iterator(); symmSetIter.hasNext();) {
            AtomSet symmSet = (AtomSet)symmSetIter.next();
            PermIter.randomPermutation(symmSetPerm, 0, symmSet.size(), rand);
            for (int atomInd=0; atomInd<symmSet.size(); atomInd++) {
            int atom = symmSet.getAtomAt(atomInd);
            // where does the i'th atom go?
            int targetInd = symmSetPerm[atomInd];
            btypePerm[atom] = symmSet.getAtomAt(targetInd);
            }
        }
        randSymm.setBasicTypePerm(btype, btypePerm);
        }  // loop over basic types
        randSymm.makeImmutable();
        sbp_.conjoin(_breakOneSymmetry(randSymm));
        numRandSymms--;
    }  // while there are more random symmetries to break
    }  // _breakRandomSymmetries()

    /**
     * Constructs a Boolean formula saying that the Alloy instance is minimal (lex-leader)
     * with respect to to the given {@link Symmetry}.  This means that we have chosen
     * a particular ordering of the Boolean variables allocated to the relations used in the
     * Alloy formula, so that each instance is a binary number obtained by writing the values
     * of the Boolean variables in that order.  A {@link Symmetry} maps instances to instances,
     * and here we construct a {@link BooleanFormula}, such that for any instance satisfying the
     * Boolean formula, the symmetry maps this instance to a lexicographically higher instance.
     * So, we construct one binary comparator, expressed as a Boolean formula.
     */
    private BooleanFormula _breakOneSymmetry(Symmetry symm_) {
        // System.out.println("BreakOneSymm: " + symm_);

        // bits of the comparator: BooleanFormulas.
        // originalBits <= permutedBits
        List /* of BooleanFormula */ originalBits = new ArrayList();
        List /* of BooleanFormula */ permutedBits = new ArrayList();
        int maxComparatorLength = Params.glob.getIntParam("SYMM","maxComparLen");

        for (Iterator relIter = _getRelationOrder().iterator();
             (maxComparatorLength==0 ||
              originalBits.size() <= maxComparatorLength) && relIter.hasNext();) {

            LeafId relId = (LeafId)relIter.next();
            ExprTransl compTransl = _relAlloc.getRelationTransl(relId);
            RelationType relType = _astInfo.getLeafType(relId);

            if (compTransl.isConstant()) continue;

            /** if no basic types of this relation are permuted
            by the symmetry, skip this relation: the symmetry has no effect
            on its bits */
            boolean skipRelation = true;
            for (int i=0; skipRelation && i<relType.numBasicTypes(); i++)
                skipRelation &= !symm_.permutes(relType.getBasicTypeAt(i));

            if (skipRelation) continue;
            // System.out.println("REL: " + _astInfo.getLeafRep(relId).nodeString());

            int[] newInds = new int[relType.numBasicTypes()];

            for (MultiDimIter indIter = new MultiDimIter(relType.getScopes());
                     indIter.hasNext();) {
                int[] oldInds = (int[])indIter.next();

                // does the symmetry fix this tuple?  if yes, skip it.  e.g. if
                // the symmetry fixes boolean variable 2 then the lex-leader condition
                // might look like 123 <= 321 which simplifies to 13<=31
                // also, compute the tuple to which the tuple oldInds is mapped
                // by symm_
                boolean thisVarFixed = true;
                for (int i=0; i<oldInds.length; i++) {
                    newInds[i] = symm_.getTargetAtom(relType.getBasicTypeAt(i), oldInds[i]);
                    thisVarFixed &= (newInds[i] == oldInds[i]);
                }
                if (thisVarFixed) continue;

                BooleanFormula originalBit = compTransl.getTupleFormula(oldInds);
                BooleanFormula permutedBit = compTransl.getTupleFormula(newInds);

                // check whether the transposition of this bit pair
                // has already been added.  if yes, this bit pair
                // has no effect, so don't add it.  if no, add it.

                boolean transpFound = false;
                for (int i=0; i<originalBits.size() && !transpFound; i++)
                    transpFound |=
                    originalBits.get(i).equals(permutedBit) &&
                    permutedBits.get(i).equals(originalBit);

                if (transpFound) continue;

                originalBits.add(originalBit);
                permutedBits.add(permutedBit);
            }   // loop over boolean variables allocated to one relation

        }  // loop over relations

        // construct the comparator
        Collections.reverse(originalBits);
        Collections.reverse(permutedBits);

        // for (int i=0; i<originalBits.size(); i++)
        //     System.out.print(" " + originalBits.get(i));
        // System.out.println(" <=");
        // for (int i=0; i<permutedBits.size(); i++)
        //     System.out.print(" " + permutedBits.get(i));
        // System.out.println("");

        IntTransl originalBitsTransl = new IntTransl((BooleanFormula[])originalBits.toArray(new BooleanFormula[]{}));
        IntTransl permutedBitsTransl = new IntTransl((BooleanFormula[])permutedBits.toArray(new BooleanFormula[]{}));
        return originalBitsTransl.ge(permutedBitsTransl).formula;
    } // _breakOneSymmetry

    /**
     * Define an ordering on all relations, which will be used in constructing lex-leader predicates.
     * Boolean variables allocated to relations that come first in the order will be used in the
     * higher-order bits of the lex-leader comparators generated in {@link #_breakOneSymmetry}.
     */
    private List /* of LeafId's of relations */ _getRelationOrder() {
	if (_relOrder != null)
	    return _relOrder;
	_relOrder = new ArrayList(_astInfo.getRelations());
	if (Params.glob.getBoolParam("SYMM", "singletonsFirst", false)) {
	    final LoneSetDetector_V loneSetDetector = new LoneSetDetector_V();
	    _astInfo.getFormula().applyVisitor(loneSetDetector);
	    Collections.sort(_relOrder, new Comparator() {
		    public int compare(Object obj1_, Object obj2_) {
			LeafId id1 = (LeafId)obj1_;
			LeafId id2 = (LeafId)obj2_;
			boolean s1 = loneSetDetector.isLoneSet(id1);
			boolean s2 = loneSetDetector.isLoneSet(id2);
			if (s1 && !s2)
			    return -1;
			if (!s1 && s2)
			    return +1;

			/* If either both are singletons or neither one is, */
			/* then sort by name then by LeafId to ensure determinism. */

			String n1 = _astInfo.getLeafRep(id1).toString();
			String n2 = _astInfo.getLeafRep(id2).toString();
			int cmpNames = n1.compareTo(n2);
			return cmpNames!=0 ? cmpNames : id1.compareTo(id2);
		    }
	    });
	}
	{
	    Dbg.info("Relation order: ");
	    for (Iterator relIter = _relOrder.iterator(); relIter.hasNext();) {
		Dbg.info(_astInfo.getLeafRep((LeafId)relIter.next()) + " ");
	    }
	    Dbg.info("");
	}
	return _relOrder;
    }

}  // class SBM_LexLeader

